Section: New Results

Formal Methods for general-purpose and domain-specific languages

Formal Semantics for Domain Specific Modeling Languages

Domain-Specific Modelling Languages (DSMLs) are languages dedicated to modelling in specific application areas. Recently, the design of DSMLs has become widely accessible to engineers trained in the basics of Model-Driven Engineering (MDE): one designs a metamodel for the language's abstract syntax; then, the language's operational semantics is expressed using model transformations over the metamodel.

The democratisation of DSML design catalysed by MDE is likely to give birth to numerous languages. One can also reasonably expect that there shall be numerous errors in those languages. Indeed, getting a language right (especially its operational semantics) is hard, regardless of whether the language is defined in the modern MDE framework or in more traditional ones.

Formal approaches can benefit language designers by helping them avoid or detect errors. But, in order to be accepted by nonexpert users, formal approaches have to operate in the background of a familiar language design process, such as the MDE-based one mentioned above.

In 2011 we have migrated from [21] , which uses the general Maude semantic framework, towards using the more language-definition specific the K-semantic framework to formalise the basic MDE ingredients used in DSML definition: models, metamodels, and model transformations. We have implemented a prototype tool that takes as input any DSML described in using MDE, and generates formal K definitions for the language's syntax, static semantics, and operational semantics. Since the definitions are executable, we get execution and formal verification engines for free [44] . A subproject of this work has been a formal definition for a substantial fragment of the OCL language [45] .

A new abstraction for signal programs, and improvement of the compilation process

In this work we propose a sound abstraction for an efficient static analysis of synchronous programs describing multi-clock embedded systems in Signal. This abstraction combines the Boolean theory and numeric interval approximation to adequately address clock relations defined as combinations of logical and numerical expressions. Through a few examples, we show how the proposed solution is used to determine absence of reaction captured by empty clocks; mutual exclusion captured by two or more clocks whose associated signals never occur at the same time; or hierarchical control of component activations via clock inclusion. We also show this analysis improves the quality of the code generated automatically by the Signal compiler, e.g., a code with smaller footprint, or a code executed more efficiently thanks to optimizations enabled by the new abstraction [38] .

Using bounded model checking to focus fixpoint iterations

Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra [40] .

A formal definition of a compiler for the Kermeta metamodeling language in K

Kermeta  [109] is a DSL designed as a kernel for metamodel engineering. It unifies metamodeling, constraints, semantics and transformation features into a statically typed language. It is object-oriented and allows for metamodeling features such as attributes, associations, and multiplicities. It also includes design-by-contract, aspect-oriented features, and genericity. This makes Kermeta a large and complex language: indeed, combining all these features into one language may easily lead to inconsistencies.

Christophe's postoctoral work, starting in September 2010, has been to formally specify Kermeta. He did so via a specification of compiler for Kermeta in K  [117] . K formal specifications are executable, hence, Christophe's compiler can be used to actually compile Kermeta programs . The compiler it completely self-contained and generates bytecode for an abstract machine also formally specified in K.

This work led to the discovery of several errors and inconsistencies in Kermeta's manual and existing interpreter. The errors are reported to the Kermeta designers (Triskell project-team at Inria Rennes-Bretagne Atlantique), who, as it turns out, are also writing a compiler of Kermeta in the traditional, informal way. We are planning to make them benefit from the experience we gained in formal compilation.

A generic approach and tool for tracing executions back to a DSML's operational semantics

Model-driven engineering allows users to define abstract syntaxes for their own DSMLs in terms of metamodels. Several approaches for defining operational semantics for DSMLs have also been proposed. These approaches allow, in principle, for model execution and for formal analyses of the DSMLs. However, most of the time, the executions/analyses are performed via transformations to other languages: code generation, resp. translation to the input language of a model checker. The consequence is that the results (e.g., a program crash log, or a counterexample returned by a model checker) may not be straightforward to interpret by the users of a DSML. We propose a formal and operational framework for tracing such results back to the original DSML's syntax and operational semantics. We implement the approach in a generic tool written in Kermeta, and illustrated in on the xSPEM language, a timed language for expressing the execution of activities constrained by time, resources, and precedences [31] .